BuiltinInfinityBadType.agda:7,22-23
Set (lsuc a) != Set a
when checking that the expression ∞ has type Set a → Set a
